\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Inductive} \coqdocvar{MatrixExp}: \coqdockw{Type} :=\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{matrix\_exp\_init} : \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{ArithExp} \ensuremath{\rightarrow} \coqdocvar{MatrixExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{matrix\_exp\_lit}  : \coqdockw{\ensuremath{\forall}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n}, \coqdocvar{Matrix} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n} \ensuremath{\rightarrow} \coqdocvar{MatrixExp}\coqdoceol
\coqdocindent{1.00em}
\ensuremath{|} \coqdocvar{matrix\_exp\_id}   : \coqdocvar{Id} \ensuremath{\rightarrow} \coqdocvar{MatrixExp}\coqdoceol
\coqdocnoindent
.\coqdoceol
\end{coqdoccode}
